w:World. FairFifo  (e:E. state_when(e)  x:Idvartype(loc(e);x)) 

latex

Definitions

f(a), EState(T), Id, , x:AB(x), t  T, state_when(e), x:A. B(x), P  Q, V(i;k), Type, kindcase(k; a.f(a); l,t.g(l;t) ), pred!(e;e'), SWellFounded(R(x;y)), loc(e), <a, b>, s = t, pred(e), first(e), b, A, loc(e), {x:A| B(x)} , , Knd, vartype(i;x), A  B, a < b, Void, False, , state_when(e), World, FairFifo, time(e), x.A(x), val(e), w-machine(w;i), t.2, t.1, #$n, s(i;t).x, w-info(w;e), w-pred(w;e), w.M, w.TA, w.T, E, S  T, IdLnk, x,y. t(x;y), x. t(x), suptype(S; T), x:A  B(x), w-automaton(T;TA;M), a(i;t), kind(a), act(e), kind(e), , x:A. B(x)

Lemmas

pred! wf, w-pred!-decreases, int-rational, nat wf, w-kind-lemma, subtype rel self, w-kind wf, w-a wf, w-machine wf, w-automaton wf, Knd wf, kindcase wf, IdLnk wf, rationals wf, w-vartype wf, fair-fifo wf, world wf, state when wf, w-T wf, w-TA wf, w-M wf, w-info wf, w-s wf, le wf, Id wf, w-time wf, not wf, assert wf, first wf, pred wf, w-pred wf, w-E wf, w-loc-pred, w-eval wf, w-loc-lemma